00100		ZERO←←274
00200		LOC ZERO
00300		PHASE	0
00400	
00500		DEFINE ABSO (N)		< N∧377 ↔ (N⊗-10)∧377 >
00600	
00700		DEFINE BRK		< 0 >
00800		DEFINE ORAIX (N)	< 1 ↔ N∧377 >
00900		DEFINE ORAZ (N)		< 5 ↔ N∧377 >
01000		DEFINE ASLZ (N)		< 6 ↔ N∧377 >
01100	
01200		DEFINE PHP		< 10 >
01300		DEFINE ORAI (N)		< 11 ↔ N∧377 >
01400		DEFINE ASLA		< 12 >
01500		DEFINE ORA (N)		< 15 ↔ N∧377 ↔ (N⊗-10)∧377 >
01600		DEFINE ASL (N)		< 16 ↔ N∧377 ↔ (N⊗-10)∧377 >
01700	
01800		DEFINE BPL (N)		< 20 ↔ (N-.-1) ∧ 377 >
01900		DEFINE ORAIY (N)	< 21 ↔ N∧377 >
02000		DEFINE ORAZX (N)	< 25 ↔ N∧377 >
02100		DEFINE ASLZX (N)	< 26 ↔ N∧377 >
02200	
02300		DEFINE CLC		< 30 >
02400		DEFINE ORAY (N)		< 31 ↔ N∧377 ↔ (N⊗-10)∧377 >
02500		DEFINE ORAX (N)		< 35 ↔ N∧377 ↔ (N⊗-10)∧377 >
02600		DEFINE ASLX (N)		< 36 ↔ N∧377 ↔ (N⊗-10)∧377 >
02700	
02800		DEFINE JSR (N)		< 40 ↔ N∧377 ↔ (N⊗-10)∧377 >
02900		DEFINE ANDIX (N)	< 41 ↔ N∧377 >
03000		DEFINE BITZ (N)		< 44 ↔ N∧377 >
03100		DEFINE ANDZ (N)		< 45 ↔ N∧377 >
03200		DEFINE ROLZ (N)		< 46 ↔ N∧377 >
     

00100		DEFINE PLP		< 50 >
00200		DEFINE ANDI (N)		< 51 ↔ N∧377 >
00300		DEFINE ROLA		< 52 >
00400		DEFINE BIT (N)		< 54 ↔ N∧377 ↔ (N⊗-10)∧377 >
00500		DEFINE AND (N)		< 55 ↔ N∧377 ↔ (N⊗-10)∧377 >
00600		DEFINE ROL (N)		< 56 ↔ N∧377 ↔ (N⊗-10)∧377 >
00700	
00800		DEFINE BMI (N)		< 60 ↔ (N-.-1) ∧ 377 >
00900		DEFINE ANDIY (N)	< 61 ↔ N∧377 >
01000		DEFINE ANDZX (N)	< 65 ↔ N∧377 >
01100		DEFINE ROLZX (N)	< 66 ↔ N∧377 >
01200	
01300		DEFINE SEC		< 70 >
01400		DEFINE ANDY (N)		< 71 ↔ N∧377 ↔ (N⊗-10)∧377 >
01500		DEFINE ANDX (N)		< 75 ↔ N∧377 ↔ (N⊗-10)∧377 >
01600		DEFINE ROLX (N)		< 76 ↔ N∧377 ↔ (N⊗-10)∧377 >
01700	
01800		DEFINE RTI		< 100 >
01900		DEFINE EORIX (N)	< 101 ↔ N∧377 >
02000		DEFINE EORZ (N)		< 105 ↔ N∧377 >
02100		DEFINE LSRZ (N)		< 106 ↔ N∧377 >
02200	
02300		DEFINE PHA		< 110 >
02400		DEFINE EORI (N)		< 111 ↔ N∧377 >
02500		DEFINE LSRA		< 112 >
02600		DEFINE JMP (N)		< 114 ↔ N∧377 ↔ (N⊗-10)∧377 >
02700		DEFINE EOR (N)		< 115 ↔ N∧377 ↔ (N⊗-10)∧377 >
02800		DEFINE LSR (N)		< 116 ↔ N∧377 ↔ (N⊗-10)∧377 >
     

00100		DEFINE BVC (N)		< 120 ↔ (N-.-1) ∧ 377 >
00200		DEFINE EORIY (N)	< 121 ↔ N∧377 >
00300		DEFINE EORZX (N)	< 125 ↔ N∧377 >
00400		DEFINE LSRZX (N)	< 126 ↔ N∧377 >
00500	
00600		DEFINE CLI		< 130 >
00700		DEFINE EORY (N)		< 131 ↔ N∧377 ↔ (N⊗-10)∧377 >
00800		DEFINE EORX (N)		< 135 ↔ N∧377 ↔ (N⊗-10)∧377 >
00900		DEFINE LSRX (N)		< 136 ↔ N∧377 ↔ (N⊗-10)∧377 >
01000	
01100		DEFINE RTS		< 140 >
01200		DEFINE ADCIX (N)	< 141 ↔ N∧377 >
01300		DEFINE ADCZ (N)		< 145 ↔ N∧377 >
01400		DEFINE RORZ (N)		< 146 ↔ N∧377 >
01500	
01600		DEFINE PLA		< 150 >
01700		DEFINE ADCI (N)		< 151 ↔ N∧377 >
01800		DEFINE RORA		< 152 >
01900		DEFINE JMPIN (N)	< 154 ↔ N∧377 ↔ (N⊗-10)∧377 >
02000		DEFINE ADC (N)		< 155 ↔ N∧377 ↔ (N⊗-10)∧377 >
02100		DEFINE ROR (N)		< 156 ↔ N∧377 ↔ (N⊗-10)∧377 >
02200	
02300		DEFINE BVS (N)		< 160 ↔ (N-.-1) ∧ 377 >
02400		DEFINE ADCIY (N)	< 161 ↔ N∧377 >
02500		DEFINE ADCZX (N)	< 165 ↔ N∧377 >
02600		DEFINE RORZX (N)	< 166 ↔ N∧377 >
     

00100		DEFINE SEI		< 170 >
00200		DEFINE ADCY (N)		< 171 ↔ N∧377 ↔ (N⊗-10)∧377 >
00300		DEFINE ADCX (N)		< 175 ↔ N∧377 ↔ (N⊗-10)∧377 >
00400		DEFINE RORX (N)		< 176 ↔ N∧377 ↔ (N⊗-10)∧377 >
00500	
00600		DEFINE STAIX (N)	< 201 ↔ N∧377 >
00700		DEFINE STYZ (N)		< 204 ↔ N∧377 >
00800		DEFINE STAZ (N)		< 205 ↔ N∧377 >
00900		DEFINE STXZ (N)		< 206 ↔ N∧377 >
01000	
01100		DEFINE DEY		< 210 >
01200		DEFINE TXA		< 212 >
01300		DEFINE STY (N)		< 214 ↔ N∧377 ↔ (N⊗-10)∧377 >
01400		DEFINE STA (N)		< 215 ↔ N∧377 ↔ (N⊗-10)∧377 >
01500		DEFINE STX (N)		< 216 ↔ N∧377 ↔ (N⊗-10)∧377 >
01600	
01700		DEFINE BCC (N)		< 220 ↔ (N-.-1) ∧ 377 >
01800		DEFINE STAIY (N)	< 221 ↔ N∧377 >
01900		DEFINE STYZX (N)	< 224 ↔ N∧377 >
02000		DEFINE STAZX (N)	< 225 ↔ N∧377 >
02100		DEFINE STXZY (N)	< 226 ↔ N∧377 >
02200	
02300		DEFINE TYA		< 230 >
02400		DEFINE STAY (N)		< 231 ↔ N∧377 ↔ (N⊗-10)∧377 >
02500		DEFINE TXS		< 232 >
02600		DEFINE STAX (N)		< 235 ↔ N∧377 ↔ (N⊗-10)∧377 >
02700	
02800		DEFINE LDYI (N)		< 240 ↔ N∧377 >
02900		DEFINE LDAIX (N)	< 241 ↔ N∧377 >
03000		DEFINE LDXI (N)		< 242 ↔ N∧377 >
03100		DEFINE LDYZ (N)		< 244 ↔ N∧377 >
03200		DEFINE LDAZ (N)		< 245 ↔ N∧377 >
03300		DEFINE LDXZ (N)		< 246 ↔ N∧377 >
     

00100		DEFINE TAY		< 250 >
00200		DEFINE LDAI (N)		< 251 ↔ N∧377 >
00300		DEFINE TAX		< 252 >
00400		DEFINE LDY (N)		< 254 ↔ N∧377 ↔ (N⊗-10)∧377 >
00500		DEFINE LDA (N)		< 255 ↔ N∧377 ↔ (N⊗-10)∧377 >
00600		DEFINE LDX (N)		< 256 ↔ N∧377 ↔ (N⊗-10)∧377 >
00700	
00800		DEFINE BCS (N)		< 260 ↔ (N-.-1) ∧ 377 >
00900		DEFINE LDAIY (N)	< 261 ↔ N∧377 >
01000		DEFINE LDYZX (N)	< 264 ↔ N∧377 >
01100		DEFINE LDAZX (N)	< 265 ↔ N∧377 >
01200		DEFINE LDXZY (N)	< 266 ↔ N∧377 >
01300	
01400		DEFINE CLV		< 270 >
01500		DEFINE LDAY (N)		< 271 ↔ N∧377 ↔ (N⊗-10)∧377 >
01600		DEFINE TSX		< 272 >
01700		DEFINE LDYX (N)		< 274 ↔ N∧377 ↔ (N⊗-10)∧377 >
01800		DEFINE LDAX (N)		< 275 ↔ N∧377 ↔ (N⊗-10)∧377 >
01900		DEFINE LDXY (N)		< 276 ↔ N∧377 ↔ (N⊗-10)∧377 >
02000	
02100		DEFINE CPYI (N)		< 300 ↔ N∧377 >
02200		DEFINE CMPIX (N)	< 301 ↔ N∧377 >
02300		DEFINE CPYZ (N)		< 304 ↔ N∧377 >
02400		DEFINE CMPZ (N)		< 305 ↔ N∧377 >
02500		DEFINE DECZ (N)		< 306 ↔ N∧377 >
02600	
02700		DEFINE INY		< 310 >
02800		DEFINE CMPI (N)		< 311 ↔ N∧377 >
02900		DEFINE DEX		< 312 >
03000		DEFINE CPY (N)		< 314 ↔ N∧377 ↔ (N⊗-10)∧377 >
03100		DEFINE CMP (N)		< 315 ↔ N∧377 ↔ (N⊗-10)∧377 >
03200		DEFINE DEC (N)		< 316 ↔ N∧377 ↔ (N⊗-10)∧377 >
     

00100		DEFINE BNE (N)		< 320 ↔ (N-.-1) ∧ 377 >
00200		DEFINE CMPIY (N)	< 321 ↔ N∧377 >
00300		DEFINE CMPZX (N)	< 325 ↔ N∧377 >
00400		DEFINE DECZX (N)	< 326 ↔ N∧377 >
00500	
00600		DEFINE CLD		< 330 >
00700		DEFINE CMPY (N)		< 331 ↔ N∧377 ↔ (N⊗-10)∧377 >
00800		DEFINE CMPX (N)		< 335 ↔ N∧377 ↔ (N⊗-10)∧377 >
00900		DEFINE DECX (N)		< 336 ↔ N∧377 ↔ (N⊗-10)∧377 >
01000	
01100		DEFINE CPXI (N)		< 340 ↔ N∧377 >
01200		DEFINE SBCIX (N)	< 341 ↔ N∧377 >
01300		DEFINE CPXZ (N)		< 344 ↔ N∧377 >
01400		DEFINE SBCZ (N)		< 345 ↔ N∧377 >
01500		DEFINE INCZ (N)		< 346 ↔ N∧377 >
01600	
01700		DEFINE INX		< 350 >
01800		DEFINE SBCI (N)		< 351 ↔ N∧377 >
01900		DEFINE NOP		< 352 >
02000		DEFINE CPX (N)		< 354 ↔ N∧377 ↔ (N⊗-10)∧377 >
02100		DEFINE SBC (N)		< 355 ↔ N∧377 ↔ (N⊗-10)∧377 >
02200		DEFINE INC (N)		< 356 ↔ N∧377 ↔ (N⊗-10)∧377 >
02300	
02400		DEFINE BEQ (N)		< 360 ↔ (N-.-1) ∧ 377 >
02500		DEFINE SBCIY (N)	< 361 ↔ N∧377 >
02600		DEFINE SBCZX (N)	< 365 ↔ N∧377 >
02700		DEFINE INCZX (N)	< 366 ↔ N∧377 >
02800	
02900		DEFINE SED		< 370 >
03000		DEFINE SBCY (N)		< 371 ↔ N∧377 ↔ (N⊗-10)∧377 >
03100		DEFINE SBCX (N)		< 375 ↔ N∧377 ↔ (N⊗-10)∧377 >
03200		DEFINE INCX (N)		< 376 ↔ N∧377 ↔ (N⊗-10)∧377 >